;;; -*- Mode: LISP; Syntax: Common-lisp; -*-

;;;; Indirect proof mechanism for LTRE
;;; Last Edited 1/29/93, by KDF

;;; Copyright (c) 1986-1993, Kenneth D. Forbus, Northwestern University,
;;; and Johan de Kleer, the Xerox Corporation.
;;; All rights reserved.

;;; See the file legal.txt for a paragraph stating scope of permission
;;; and disclaimer of warranty.  The above copyright notice and that
;;; paragraph must be included in any separate copy of this file.

(defpackage #:bps/ltms/indirect
  (:use #:cl
        #:bps/ltms/ltms
        #:bps/ltms/linter
        #:bps/ltms/ldata
        #:bps/ltms/lrules)
  (:export
   #:try-indirect-proof))

(in-package #:bps/ltms/indirect)

(proclaim '(special *LTRE*))

(defun try-indirect-proof (fact &optional (*LTRE* *LTRE*))
  (unless (known? fact)
    (with-contradiction-handler (ltre-ltms *ltre*)
        #'(lambda (contradictions ltms &aux assumptions)
            (declare (ignore ltms))
            (setq assumptions
                  (assumptions-of-clause
                   (car contradictions)))
            (let ((the-node
                   (find (datum-tms-node (referent fact T))
                         assumptions)))
              (when the-node
                (let ((status (tms-node-label the-node)))
                  (retract-assumption the-node)
                  (add-nogood the-node status
                              assumptions)))))
      ;; Assume the negation
      (assuming `((:NOT ,fact)) *LTRE*
        (run-rules)))
    (known? fact)))

;;;; Example of indirect proof

(defun indirect-proof-example ()
  (in-ltre (create-ltre "Indirect Proof Example"))
  (assert! '(:OR p q) 'user)
  (assert! '(:IMPLIES p r) 'user)
  (assert! '(:IMPLIES q r) 'user)
  (known? 'r)
  (try-indirect-proof 'r)
  (known? 'r))
